/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#3=SUB/FONT#4=SUP/FONT#5=GACS25/FONT#6=FIX20/FONT#7=SYMB30[FNT,CLT]/FONT#8=FIX25/FONT#11=GRFX25/FONT#12=GRFX35/FONT#9=BEESIX















␈↓ ↓H␈↓	␈↓ ε≥LISP


␈↓ ↓H␈↓	␈↓ ∧eProgramming and Proving




␈↓ ↓H␈↓	␈↓ ¬∪CHAPTER COMPUT










␈↓ ↓H␈↓␈↓ ¬SCopyright ␈↓π@␈↓ 1980

␈↓ ↓H␈↓␈↓ ∧XJohn McCarthy and Carolyn Talcott


␈↓ ↓H␈↓␈↓ ¬GStanford University



␈↓ ↓H␈↓␈↓ ∧¬This version printed at 17:02 on August 24, 1980.
␈↓ ↓H␈↓␈↓ εH␈↓ ?i


␈↓ ↓H␈↓α␈↓ ¬NTable of Contents



␈↓ ↓H␈↓␈↓ 	Page



␈↓ ↓H␈↓XI␈↓ α_COMPUTABILITY

␈↓ ↓H␈↓␈↓ α81␈↓ αxA Call-by-name LISP interpreter.␈↓ ε8   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .␈↓ ≠   1

␈↓ ↓H␈↓␈↓ α82␈↓ αxNon-computability.␈↓ ∧x   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .␈↓ ≠   2

␈↓ ↓H␈↓␈↓ α83␈↓ αxLambda calculus␈↓ ∧x   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .␈↓ ≠   4


␈↓ ↓H␈↓FUNCTION INDEX


␈↓ ↓H␈↓DEFINED LABELS
␈↓ ↓H␈↓␈↓ εH␈↓ 91


␈↓ ↓H␈↓α␈↓ ¬{Chapter XI

␈↓ ↓H␈↓α␈↓ ¬BCOMPUTABILITY




␈↓ ↓H␈↓1.  ␈↓αA Call-by-name LISP interpreter.␈↓


␈↓ ↓H␈↓        Except␈αfor␈αspeed␈αand␈αmemory␈αsize␈αall␈αpresent␈αday␈αstored␈αprogram␈αcomputers␈αare␈αequivalent
␈↓ ↓H␈↓in␈αwhat␈αcomputations␈αthey␈αcan␈αdo.␈α A␈αprogram␈αwritten␈αfor␈αone␈αcomputer␈αcan␈αbe␈αtranslated␈αto␈αrun
␈↓ ↓H␈↓on␈αanother.␈α Indeed,␈αone␈αcan␈αwrite␈αa␈αsimulator␈αfor␈αone␈αcomputer␈αto␈αrun␈αon␈αanother.␈α To␈αput␈αit␈αin
␈↓ ↓H␈↓commercial␈α
terms,␈α
no␈α
computer␈α
manufacturer␈α
can␈α
advertise␈α
that␈α
his␈α
machine␈α
can␈α
do␈αcalculations
␈↓ ↓H␈↓impossible on the machine made by his competitors.

␈↓ ↓H␈↓        This␈αis␈αwell␈αknown␈αintuitively,␈αand␈αthe␈αfirst␈αmathematical␈αtheorem␈αof␈αthis␈αkind␈αwas␈αproved
␈↓ ↓H␈↓by␈αA.M.␈αTuring␈α(1936),␈αwho␈αdefined␈αa␈αprimitive␈αkind␈αof␈αcomputer␈αnow␈αcalled␈αa␈αTuring␈αmachine,
␈↓ ↓H␈↓and␈α⊃showed␈α⊃how␈α⊃to␈α⊃make␈α⊂a␈α⊃universal␈α⊃machine␈α⊃that␈α⊃could␈α⊂do␈α⊃any␈α⊃computation␈α⊃done␈α⊃by␈α⊂any
␈↓ ↓H␈↓Turing␈αmachine␈αwhen␈αgiven␈αa␈αdescription␈αof␈αthe␈αmachine␈αto␈αbe␈αsimulated␈αand␈αthe␈αinitial␈αtape␈αof
␈↓ ↓H␈↓the computation to be imitated.

␈↓ ↓H␈↓        In␈α∂LISP␈α∂the␈α∂function␈α∂␈↓↓eval,␈↓␈α∂defined␈α∂in␈α⊂Chapter I␈α∂()␈α∂is␈α∂a␈α∂universal␈α∂LISP␈α∂function␈α⊂in␈α∂the
␈↓ ↓H␈↓sense␈α
that␈α
any␈α
computation␈α
done␈αby␈α
any␈α
LISP␈α
function␈α
can␈α
be␈αdone␈α
by␈α
␈↓↓eval␈↓␈α
when␈α
␈↓↓eval␈↓␈α
is␈αgiven
␈↓ ↓H␈↓suitable arguments.

␈↓ ↓H␈↓        The␈α⊂way␈α⊂␈↓↓eval␈↓␈α⊂handles␈α⊂arguments␈α∂corresponds␈α⊂to␈α⊂the␈α⊂call-by-value␈α⊂method␈α⊂of␈α∂parameter
␈↓ ↓H␈↓passing␈αin␈αALGOL␈αand␈αsimilar␈αlanguages.␈α There␈αis␈αalso␈αa␈αform␈αof␈α␈↓↓eval␈↓␈αthat␈αcorresponds␈αto␈αcall-
␈↓ ↓H␈↓by-name.␈α∞ The␈α
practical␈α∞difference␈α
between␈α∞call-by-value␈α
and␈α∞call-by-name␈α
is␈α∞that␈α∞sometimes␈α
a
␈↓ ↓H␈↓function␈α⊂doesn't␈α⊂need␈α⊂all␈α⊂its␈α⊂arguments,␈α⊂because␈α⊂the␈α⊂values␈α⊂of␈α⊂some␈α⊂arguments␈α⊂may␈α⊂make␈α⊂the
␈↓ ↓H␈↓evaluation␈α
of␈α
others␈α
unnecessary.␈α A␈α
trivial␈α
example␈α
is␈αthat␈α
if␈α
␈↓↓x␈↓␈α
is␈α
0,␈αthen␈α
the␈α
value␈α
of␈αthe␈α
product
␈↓ ↓H␈↓␈↓↓xy␈↓␈αcan␈αbe␈αdetermined␈αwithout␈αevaluating␈α␈↓↓y.␈↓␈α Other␈αexamples␈αinvolve␈αconditional␈αexpressions.␈α In
␈↓ ↓H␈↓call-by-value,␈α⊂a␈α∂subfunction␈α⊂is␈α⊂given␈α∂the␈α⊂values␈α⊂of␈α∂its␈α⊂arguments,␈α⊂while␈α∂in␈α⊂call-by-name,␈α⊂it␈α∂is
␈↓ ↓H␈↓given␈αthe␈αlocation␈αof␈αprogram␈αfor␈αcomputing␈αthem␈αand␈αcan␈αdecide␈αwhich␈αit␈αwants␈αto␈αcompute.␈α If
␈↓ ↓H␈↓this␈αwere␈αall␈αthere␈αis␈αto␈αsay,␈αcall-by-name␈αwould␈αclearly␈αbe␈αsuperior.␈α However,␈αin␈αstraightforward
␈↓ ↓H␈↓call-by-name,␈α∞it␈α∞can␈α∞happen␈α∞that␈α
an␈α∞argument␈α∞that␈α∞is␈α∞used␈α
in␈α∞two␈α∞different␈α∞places␈α∞is␈α
computed
␈↓ ↓H␈↓twice,␈α∩and␈α∩there␈α⊃are␈α∩other␈α∩problems.␈α⊃ LISP␈α∩uses␈α∩call-by-value,␈α⊃perhaps␈α∩mainly␈α∩for␈α⊃historical
␈↓ ↓H␈↓reasons, but it also has some advantages.

␈↓ ↓H␈↓        Here is a call-by-name ␈↓↓eval␈↓ called ␈↓↓neval:␈↓

␈↓ ↓H␈↓␈↓ α8␈↓↓        neval[e, a] ← ␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓        ␈↓αif␈↓↓ ␈↓αat|␈↓↓e ␈↓αthen␈↓↓␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                [␈↓αif␈↓↓ e = ␈↓¬T␈↓↓  ␈↓αthen␈↓↓ ␈↓¬T␈↓↓␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                ␈↓αelse␈↓↓ ␈↓αif␈↓↓ e = ␈↓¬NIL␈↓↓ ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                ␈↓αelse␈↓↓ ␈↓αif␈↓↓ numberp e ␈↓αthen␈↓↓ e␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                ␈↓αelse␈↓↓ neval[␈↓αad|␈↓↓assoc[e, a], ␈↓αdd|␈↓↓assoc[e, a]]]␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓        ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αat|␈↓↓␈↓αa|␈↓↓e ␈↓αthen␈↓↓␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                [␈↓αif␈↓↓ ␈↓αa|␈↓↓e = ␈↓¬CAR ␈↓↓␈↓αthen␈↓↓ ␈↓αa|␈↓↓neval[␈↓αad|␈↓↓e, a]␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa|␈↓↓e = ␈↓¬CDR ␈↓↓␈↓αthen␈↓↓ ␈↓αd|␈↓↓neval[␈↓αad|␈↓↓e, a]␈↓
␈↓ ↓H␈↓1.1)␈↓ α8␈↓↓             ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa|␈↓↓e = ␈↓¬CONS ␈↓↓␈↓αthen␈↓↓ neval[␈↓αad|␈↓↓e, a] . neval[␈↓αadd|␈↓↓e, a]␈↓
␈↓ ↓H␈↓␈↓ ¬wChapter  XI␈↓ 92


␈↓ ↓H␈↓␈↓ α8␈↓↓                ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa|␈↓↓e = ␈↓¬ATOM ␈↓↓␈↓αthen␈↓↓ ␈↓αat|␈↓↓neval[␈↓αad|␈↓↓e, a]␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa|␈↓↓e = ␈↓¬EQ ␈↓↓␈↓αthen␈↓↓ neval[␈↓αad|␈↓↓e, a] = neval[␈↓αadd|␈↓↓e, a]␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa|␈↓↓e = ␈↓¬QUOTE ␈↓↓␈↓αthen␈↓↓ ␈↓αad|␈↓↓e␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa|␈↓↓e = ␈↓¬COND ␈↓↓␈↓αthen␈↓↓ nevcon[␈↓αd|␈↓↓e, a]␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa|␈↓↓e = ␈↓¬LIST ␈↓↓␈↓αthen␈↓↓ mapcar[␈↓αd|␈↓↓e, λx: neval[x, a]]␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓                ␈↓αelse␈↓↓ neval[␈↓αd|␈↓↓assoc[␈↓αa|␈↓↓e, a] . ␈↓αd|␈↓↓e, a]]␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓        ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αaa|␈↓↓e = ␈↓¬LAMBDA ␈↓↓␈↓αthen␈↓↓ neval[␈↓αadda|␈↓↓e, nprup[␈↓αada|␈↓↓e, ␈↓αd|␈↓↓e,  a]]␈↓
␈↓ ↓H␈↓␈↓ α8␈↓↓        ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αaa|␈↓↓e = ␈↓¬LABEL ␈↓↓␈↓αthen␈↓↓ neval[␈↓αadda|␈↓↓e . ␈↓αd|␈↓↓e, [␈↓αada|␈↓↓e . ␈↓αa|␈↓↓e] . a]␈↓,

␈↓ ↓H␈↓where the auxiliary function ␈↓↓nevcon␈↓ is given by

␈↓ ↓H␈↓1.2)␈↓ αp␈↓↓nevcon[u, a] ← ␈↓αif␈↓↓ neval[␈↓αaa|␈↓↓u, a] ␈↓αthen␈↓↓ neval[␈↓αada|␈↓↓u, a] ␈↓αelse␈↓↓ nevcon[␈↓αd|␈↓↓u, a]␈↓. 

␈↓ ↓H␈↓and ␈↓↓nprup␈↓ is

␈↓ ↓H␈↓1.3)␈↓ αy␈↓↓nprup[u, v,a] ← ␈↓αif␈↓↓ ␈↓αn|␈↓↓u ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ [␈↓αa|␈↓↓u . [␈↓αa|␈↓↓v . a]] . nprup[␈↓αd|␈↓↓u, ␈↓αd|␈↓↓v,a]␈↓. 

␈↓ ↓H␈↓        The␈α
difference␈α
between␈α∞␈↓↓eval␈↓␈α
and␈α
␈↓↓neval␈↓␈α
is␈α∞only␈α
in␈α
two␈α
terms.␈α∞ ␈↓↓eval␈↓␈α
evaluates␈α
a␈α∞variable␈α
by
␈↓ ↓H␈↓looking␈αit␈αup␈αon␈αthe␈αassociation␈αlist␈αwhereas␈α
␈↓↓neval␈↓␈αlooks␈αit␈αup␈αon␈αthe␈αassociation␈αlist␈αand␈α
evaluates
␈↓ ↓H␈↓the␈αresult␈αin␈αthe␈αcontext␈αin␈αwhich␈αit␈αwas␈αput␈αon␈αthe␈αassociation␈αlist.␈α Correspondingly,␈αwhen␈αa␈αλ-
␈↓ ↓H␈↓expression␈α
is␈αencountered,␈α
␈↓↓eval␈↓␈α
forms␈αa␈α
new␈α
association␈αlist␈α
by␈α
pairing␈αthe␈α
values␈α
of␈αthe␈α
arguments
␈↓ ↓H␈↓with␈αthe␈α
variables␈αbound␈αby␈α
the␈αλ␈αand␈α
putting␈αthe␈αnew␈α
pairs␈αin␈αfront␈α
of␈αthe␈αold␈α
association␈αlist,
␈↓ ↓H␈↓whereas␈α
␈↓↓neval␈↓␈α
pairs␈α
the␈α
arguments␈α
themselves␈α
with␈αthe␈α
variables␈α
and␈α
puts␈α
them␈α
on␈α
the␈α
front␈αof
␈↓ ↓H␈↓the␈α
association␈αlist.␈α
 The␈α
function␈α␈↓↓neval␈↓␈α
also␈α
saves␈αthe␈α
current␈α
association␈αlist␈α
with␈α
each␈αvariable
␈↓ ↓H␈↓on␈αthe␈αassociation␈αlist,␈αso␈αthat␈αthe␈αvariables␈αcan␈αbe␈αevaluated␈αin␈αthe␈αcorrect␈αcontext.␈α In␈αmost␈αcases
␈↓ ↓H␈↓they␈α⊂give␈α∂the␈α⊂same␈α∂result␈α⊂with␈α∂the␈α⊂same␈α∂work,␈α⊂but␈α∂␈↓↓neval␈↓␈α⊂gives␈α∂a␈α⊂result␈α∂for␈α⊂some␈α⊂functions␈α∂of
␈↓ ↓H␈↓several␈αarguments␈αfor␈αwhich␈α␈↓↓eval␈↓␈αloops.␈α An␈αexample␈αis␈αobtained␈αby␈αevaluating␈α␈↓↓F[2,␈α1]␈↓␈αwhere␈α␈↓↓F␈↓
␈↓ ↓H␈↓is defined by

␈↓ ↓H␈↓␈↓ ∧
␈↓↓F[x, y] ← ␈↓αif␈↓↓ x=0 ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ F[x-1, F[y-2, x]]␈↓. 

␈↓ ↓H␈↓        Vuillemin␈α
[1973]␈α
showed␈α
that␈α
if␈α
a␈α
function␈α
is␈α
␈↓↓strict,␈↓␈α
never␈α
has␈α
a␈α
defined␈α
value␈α
unless␈α
all
␈↓ ↓H␈↓arguments have a defined value, then call-by-name and call-by-value always give the same result.


␈↓ ↓H␈↓α␈↓ ε
Exercises

␈↓ ↓H␈↓1.␈α⊂Write␈α⊃␈↓↓neval␈↓␈α⊂and␈α⊂the␈α⊃necessary␈α⊂auxiliary␈α⊃functions␈α⊂in␈α⊂list␈α⊃form,␈α⊂and␈α⊂try␈α⊃them␈α⊂out␈α⊃on␈α⊂some
␈↓ ↓H␈↓examples.



␈↓ ↓H␈↓2.  ␈↓αNon-computability.␈↓


␈↓ ↓H␈↓        Some␈α∞LISP␈α
calculations␈α∞run␈α∞on␈α
indefinitely.␈α∞ The␈α∞most␈α
trivial␈α∞case␈α∞occurs␈α
if␈α∞we␈α∞make␈α
the
␈↓ ↓H␈↓recursive definition

␈↓ ↓H␈↓2.1)␈↓ ¬(␈↓↓loop x ← loop x             ␈↓ 
␈↓ ↓H␈↓␈↓ ¬wChapter  XI␈↓ 93


␈↓ ↓H␈↓and␈α
attempt␈α
to␈α
compute␈α
␈↓↓loop[x]␈↓␈α
for␈α
any␈α
␈↓↓x␈↓␈α
whatsoever.␈α
 Don't␈α
dismiss␈α
this␈α
example␈α
just␈αbecause␈α
no-
␈↓ ↓H␈↓one␈αwould␈αwrite␈αsuch␈αan␈αobviously␈αuseless␈αfunction␈αdefinition.␈α There␈αis␈αa␈αsense␈αin␈αwhich␈αit␈αis␈α
the
␈↓ ↓H␈↓"zero"␈α∞of␈α∞a␈α
large␈α∞class␈α∞of␈α
non-terminating␈α∞function␈α∞definitions,␈α
and,␈α∞as␈α∞the␈α∞Romans␈α
experienced
␈↓ ↓H␈↓but never learned, leaving zero out of the number system is a mistake.

␈↓ ↓H␈↓        Nevertheless,␈αin␈αmost␈α
programming,␈αnon-terminating␈αcalculations␈αare␈α
the␈αresults␈αof␈αerrors␈α
in
␈↓ ↓H␈↓defining␈αfunctions.␈α Therefore,␈αit␈αwould␈αbe␈αuseful␈αto␈αbe␈αable␈αto␈αtell␈αwhether␈αa␈αfunction␈αdefinition
␈↓ ↓H␈↓gives␈αa␈αresult␈α
for␈αall␈αarguments.␈α In␈α
fact,␈αit␈αwould␈αbe␈α
useful␈αto␈αbe␈αable␈α
to␈αtell␈αwhether␈α
a␈αfunction
␈↓ ↓H␈↓will terminate for a single argument.  Let us make this goal more precise.

␈↓ ↓H␈↓        Suppose␈α∞that␈α
␈↓↓f␈↓␈α∞is␈α∞a␈α
LISP␈α∞function␈α∞and␈α
␈↓↓a␈↓␈α∞is␈α∞an␈α
S-expression,␈α∞and␈α∞we␈α
would␈α∞like␈α∞to␈α
know
␈↓ ↓H␈↓whether␈α
the␈α
computation␈αof␈α
␈↓↓f[a]␈↓␈α
terminates.␈α
 Suppose␈α␈↓↓f␈↓␈α
is␈α
represented␈αby␈α
the␈α
S-expression␈α
␈↓↓f*␈↓␈αin
␈↓ ↓H␈↓internal␈α∞notation.␈α
 Then␈α∞the␈α
S-expression␈α∞␈↓¬(␈↓↓f*␈↓¬␈α
(QUOTE␈α∞␈↓↓a␈↓¬))␈↓␈α
represents␈α∞␈↓↓f[a].␈↓␈α
 Define␈α∞the␈α
function
␈↓ ↓H␈↓␈↓↓term␈↓␈α∞by␈α∞giving␈α∞␈↓↓term[e]␈↓␈α∂the␈α∞value␈α∞␈↓αtrue␈↓␈α∞if␈α∂␈↓↓e␈↓␈α∞is␈α∞an␈α∞S-expression␈α∞of␈α∂the␈α∞form␈α∞␈↓¬(␈↓↓f*␈↓¬␈α∞(QUOTE␈α∂␈↓↓a␈↓¬))␈↓␈α∞for
␈↓ ↓H␈↓which␈α␈↓↓f[a]␈↓␈αterminates␈αand␈α␈↓αfalse␈↓␈αotherwise.␈α We␈αnow␈αask␈αwhether␈α␈↓↓term␈↓␈αis␈αa␈αLISP␈αfunction,␈αi.e.␈αcan
␈↓ ↓H␈↓it␈αbe␈αconstructed␈α
from␈α␈↓↓car,␈↓␈α␈↓↓cdr,␈↓␈α␈↓↓cons,␈↓␈α
␈↓↓atom,␈↓␈α and␈α␈↓↓eq␈↓␈αusing␈α
␈↓↓λ,␈↓␈α␈↓↓label,␈↓␈αand␈αconditional␈α
expressions?
␈↓ ↓H␈↓Well,␈αit␈αcan't,␈αas␈αwe␈αshall␈αshortly␈αprove,␈αand␈αthis␈αmeans␈αthat␈αit␈αis␈αnot␈α␈↓↓computable␈↓␈αwhether␈αa␈αLISP
␈↓ ↓H␈↓calculation␈αterminates,␈αsince␈αif␈α␈↓↓term␈↓␈αwere␈αcomputable␈αby␈αany␈αcomputer␈αor␈αin␈αany␈αrecognized␈αsense,
␈↓ ↓H␈↓it could be represented as a LISP function.  Here is the proof:

␈↓ ↓H␈↓        Consider the function ␈↓↓terma␈↓ defined from ␈↓↓term␈↓ by

␈↓ ↓H␈↓2.2)␈↓ β2␈↓↓terma u ← ␈↓αif␈↓↓ term list[u, list[␈↓¬QUOTE, ␈↓↓u]] ␈↓αthen␈↓↓ loop u ␈↓αelse␈↓↓ ␈↓αtrue␈↓↓␈↓, 

␈↓ ↓H␈↓and␈α∞suppose␈α∞that␈α∞␈↓↓f␈↓␈α∞is␈α∞a␈α∞LISP␈α∞function␈α
and␈α∞that␈α∞␈↓↓f*␈↓␈α∞is␈α∞its␈α∞S-expression␈α∞representation.␈α∞ What␈α
is
␈↓ ↓H␈↓␈↓↓terma␈↓␈α␈↓↓f*␈↓␈α?␈αWell␈α␈↓↓terma␈↓␈α␈↓↓f*␈↓␈αtells␈αus␈αwhether␈αthe␈αcomputation␈αof␈α␈↓↓f[f*]␈↓␈αterminates,␈αand␈αit␈αtells␈αus␈αthis
␈↓ ↓H␈↓by␈α∞going␈α∂into␈α∞a␈α∂loop␈α∞if␈α∂␈↓↓f[f*]␈↓␈α∞terminates␈α∂and␈α∞giving␈α∂␈↓αtrue␈↓␈α∞otherwise.␈α∂ Now␈α∞if␈α∂␈↓↓term␈↓␈α∞were␈α∂a␈α∞LISP
␈↓ ↓H␈↓function,␈α
then␈α
␈↓↓terma␈↓␈α
would␈αalso␈α
be␈α
a␈α
LISP␈αfunction.␈α
 Indeed␈α
if␈α
␈↓↓term␈↓␈αwere␈α
represented␈α
by␈α
the␈αS-
␈↓ ↓H␈↓expression ␈↓↓term*,␈↓ then ␈↓↓terma␈↓ would be represented by the S-expression

␈↓ ↓H␈↓2.3)␈↓ ↓m␈↓↓terma*␈↓ = ␈↓¬(LAMBDA (U) (COND ((␈↓↓term*␈↓¬ (LIST U (LIST (QUOTE QUOTE) U))) (LOOP U)) 
␈↓ ↓H␈↓ ε
␈↓¬(T T)))␈↓. 

␈↓ ↓H␈↓Now␈α⊂consider␈α∂␈↓↓terma[terma*].␈↓␈α⊂  According␈α∂to␈α⊂the␈α∂definition␈α⊂of␈α∂␈↓↓terma,␈↓␈α⊂this␈α∂will␈α⊂tell␈α⊂us␈α∂whether
␈↓ ↓H␈↓␈↓↓terma[terma*]␈↓␈αis␈αdefined,␈αi.e.␈αit␈αtells␈αabout␈αitself.␈α However,␈αit␈αgives␈αthis␈αanswer␈αin␈αa␈αcontradictory
␈↓ ↓H␈↓way;␈α
namely␈α␈↓↓terma[terma*]␈↓␈α
looping␈α
tells␈αus␈α
that␈α
␈↓↓terma[terma*]␈↓␈αterminates,␈α
and␈α␈↓↓terma[terma*]␈↓␈α
being
␈↓ ↓H␈↓␈↓αtrue␈↓␈α∞tells␈α∞us␈α
that␈α∞␈↓↓terma[terma*]␈↓␈α∞doesn't␈α∞terminate.␈α
 This␈α∞contradiction␈α∞tells␈α∞us␈α
that␈α∞␈↓↓term␈↓␈α∞is␈α∞not␈α
a
␈↓ ↓H␈↓LISP␈α∃function,␈α∃and␈α∃there␈α∃is␈α∃no␈α∀general␈α∃procedure␈α∃for␈α∃telling␈α∃whether␈α∃a␈α∃LISP␈α∀calculation
␈↓ ↓H␈↓terminates.

␈↓ ↓H␈↓        The␈α∩above␈α⊃result␈α∩does␈α⊃not␈α∩exclude␈α⊃LISP␈α∩functions␈α⊃that␈α∩tell␈α⊃whether␈α∩LISP␈α⊃calculations
␈↓ ↓H␈↓terminate.␈α⊃ It␈α⊃just␈α⊃excludes␈α∩perfect␈α⊃ones.␈α⊃ Suppose␈α⊃we␈α⊃have␈α∩a␈α⊃function␈α⊃␈↓↓t␈↓␈α⊃that␈α∩sometimes␈α⊃says
␈↓ ↓H␈↓calculations␈α∂terminate,␈α∞sometimes␈α∂says␈α∂they␈α∞don't␈α∂terminate,␈α∂and␈α∞sometimes␈α∂runs␈α∂on␈α∞indefinitely.
␈↓ ↓H␈↓We␈α
shall␈α
further␈α
assume␈α
that␈α
when␈α
␈↓↓t␈↓␈α
gives␈αan␈α
answer␈α
it␈α
is␈α
always␈α
right.␈α
 Given␈α
such␈α
a␈αfunction␈α
we
␈↓ ↓H␈↓can␈αimprove␈αit␈α
a␈αbit␈αso␈α
that␈αit␈αwill␈α
always␈αgive␈αthe␈α
right␈αanswer␈αwhen␈α
the␈αcalculation␈αit␈α
is␈αasked
␈↓ ↓H␈↓about␈α∪terminates.␈α∪ This␈α∀is␈α∪done␈α∪by␈α∀mixing␈α∪the␈α∪computation␈α∪of␈α∀␈↓↓t[e]␈↓␈α∪with␈α∪a␈α∀computation␈α∪of
␈↓ ↓H␈↓␈↓↓eval[e, ␈↓¬NIL␈↓↓]␈↓␈αdoing␈αthe␈αcomputations␈αalternately.␈α If␈αthe␈α␈↓↓eval[e, ␈↓¬NIL␈↓↓]␈↓␈αcomputation␈αever␈αterminates,
␈↓ ↓H␈↓then the new function asserts termination.

␈↓ ↓H␈↓        Given␈αsuch␈αa␈α␈↓↓t,␈↓␈αwe␈αcan␈αalways␈αfind␈αa␈αcalculation␈αthat␈αdoes␈αnot␈αterminate␈αbut␈α␈↓↓t␈↓␈αdoesn't␈αsay
␈↓ ↓H␈↓so.  The construction is just like that used in the previous proof.  Given ␈↓↓t,␈↓ we construct
␈↓ ↓H␈↓␈↓ ¬wChapter  XI␈↓ 94


␈↓ ↓H␈↓2.4) ␈↓ β`␈↓↓ta u ← ␈↓αif␈↓↓ t list[u, list[␈↓¬QUOTE, ␈↓↓u]] ␈↓αthen␈↓↓ loop u ␈↓αelse␈↓↓ ␈↓αtrue␈↓↓␈↓, 

␈↓ ↓H␈↓and␈α
then␈α
we␈α
consider␈α
␈↓↓ta[ta*].␈↓␈α
 If␈α
this␈α
had␈α
the␈α
value␈α
␈↓αtrue␈↓,␈α
then␈α
it␈α
wouldn't␈α
terminate␈α
so␈α
therefore␈α
it
␈↓ ↓H␈↓doesn't␈α⊃terminate␈α⊃but␈α⊂is␈α⊃not␈α⊃one␈α⊂of␈α⊃those␈α⊃expressions␈α⊂which␈α⊃␈↓↓t␈↓␈α⊃decides.␈α⊂ Thus␈α⊃for␈α⊃any␈α⊂partial
␈↓ ↓H␈↓decider␈α∂we␈α∂can␈α∞find␈α∂a␈α∂LISP␈α∂calculation␈α∞which␈α∂doesn't␈α∂terminate␈α∞but␈α∂which␈α∂the␈α∂decider␈α∞doesn't
␈↓ ↓H␈↓decide.  This can in turn be used to get a slightly better decider, namely

␈↓ ↓H␈↓2.5)␈↓ βj␈↓↓t␈↓β1␈↓↓[e] ← ␈↓αif␈↓↓ e = ta* ␈↓αthen␈↓↓ ␈↓¬DOESN'T-TERMINATE ␈↓↓ ␈↓αelse␈↓↓ t[e]␈↓. 

␈↓ ↓H␈↓Of␈αcourse,␈α␈↓↓t␈↓␈↓β1␈↓␈αisn't␈αmuch␈αbetter␈αthan␈α␈↓↓t,␈↓␈αsince␈αit␈αcan␈αdecide␈αonly␈αone␈αmore␈αcomputation,␈αbut␈αwe␈αcan
␈↓ ↓H␈↓form␈α␈↓↓t␈↓␈↓β2␈↓␈αby␈αapplying␈αthe␈αsame␈αprocess,␈αand␈αso␈αforth.␈α In␈αfact,␈αwe␈αcan␈αeven␈αform␈α␈↓↓t␈↓␈↓π␈↓#vw␈↓#␈↓␈αwhich␈αdecides
␈↓ ↓H␈↓all␈αthe␈αcases␈αdecided␈αby␈αany␈α␈↓↓t␈↓␈↓βn␈↓.␈α This␈αcan␈αbe␈αfurther␈αimproved␈αby␈αthe␈αsame␈αprocess,␈αetc.␈α How␈αfar
␈↓ ↓H␈↓can␈α∂we␈α∂go?␈α∞ The␈α∂answer␈α∂is␈α∞technical;␈α∂namely,␈α∂the␈α∞improvement␈α∂process␈α∂can␈α∞be␈α∂carried␈α∂out␈α∞any
␈↓ ↓H␈↓recursive ordinal number of times.

␈↓ ↓H␈↓        Unfortunately,␈α⊂this␈α⊂kind␈α∂of␈α⊂improvement␈α⊂seems␈α∂to␈α⊂be␈α⊂superficial,␈α∂since␈α⊂none␈α⊂of␈α⊂the␈α∂new
␈↓ ↓H␈↓computations proved not to terminate are likely to be of practical interest.


␈↓ ↓H␈↓α␈↓ ε
Exercises

␈↓ ↓H␈↓1. Write a function that gives ␈↓↓t␈↓␈↓βn+1␈↓ in terms of ␈↓↓t␈↓␈↓βn␈↓.

␈↓ ↓H␈↓2. Write a function that gives ␈↓↓t␈↓␈↓π␈↓#vw␈↓#␈↓ in terms of ␈↓↓t.␈↓

␈↓ ↓H␈↓3.␈α∞If␈α∞you␈α∞know␈α∞about␈α
Turing␈α∞machines,␈α∞write␈α∞a␈α∞LISP␈α
function␈α∞to␈α∞simulate␈α∞an␈α∞arbitrary␈α
Turing
␈↓ ↓H␈↓machine given a description of the machine in some convenient notation.

␈↓ ↓H␈↓4.␈α
Write␈α
a␈α
LISP␈α
function␈αthat␈α
will␈α
translate␈α
a␈α
Turing␈αmachine␈α
description␈α
into␈α
a␈α
LISP␈αfunction
␈↓ ↓H␈↓that will do the same computation.

␈↓ ↓H␈↓5.␈αIf␈αyou␈αreally␈αlike␈αTuring␈αmachines,␈αwrite␈αa␈αdescription␈αof␈αa␈αTuring␈αmachine␈αthat␈αwill␈αinterpret
␈↓ ↓H␈↓LISP internal notation.



␈↓ ↓H␈↓3.  ␈↓αLambda calculus␈↓


␈↓ ↓H␈↓        The␈α⊃lambda␈α⊂notation␈α⊃used␈α⊃in␈α⊂LISP␈α⊃was␈α⊂taken␈α⊃from␈α⊃the␈α⊂lambda␈α⊃calculus␈α⊃developed␈α⊂by
␈↓ ↓H␈↓Alonzo␈α∪Church␈α∪in␈α∪the␈α∪late␈α∩1920s␈α∪and␈α∪described␈α∪in␈α∪his␈α∩1940␈α∪book,␈α∪␈↓↓The␈α∪Calculi␈α∪of␈α∩Lambda
␈↓ ↓H␈↓↓Conversion␈↓.␈α This␈αsection␈αcovers␈αsome␈αaspects␈αof␈αthe␈αlambda␈αcalculus␈αthat␈αgo␈αbeyond␈αwhat␈αis␈αused
␈↓ ↓H␈↓in LISP.

␈↓ ↓H␈↓        Each␈α
LISP␈α
expression␈α
either␈α
evaluates␈α
to␈α
some␈α
object␈α
(like␈α
␈↓↓␈↓αa|␈↓↓x␈↓)␈α
or␈α
it␈α
represents␈α∞a␈α
function
␈↓ ↓H␈↓(like␈α␈↓↓λx.[␈↓αa|␈↓↓x . y]␈↓).␈α [In␈αthe␈αterminology␈αof␈αlogic,␈αit␈αhas␈αa␈αdefinite␈αtype,␈αbut␈αthe␈αword␈α"type"␈αis␈αoften
␈↓ ↓H␈↓used␈αdifferently␈αin␈αcomputer␈αscience␈αwhere␈αnumbers␈αand␈αlist␈αstructure␈αare␈αconsidered␈αof␈αdifferent
␈↓ ↓H␈↓types.␈α∂ Logicians␈α∂use␈α∂the␈α∂word␈α∂"sort"␈α⊂for␈α∂the␈α∂computer␈α∂scientist's␈α∂"type"].␈α∂ The␈α⊂lambda␈α∂calculus
␈↓ ↓H␈↓doesn't make this distinction, and any expression can be taken as a function.
␈↓ ↓H␈↓␈↓ ¬wChapter  XI␈↓ 95


␈↓ ↓H␈↓        Lambda␈α⊂calculus␈α⊂is␈α⊂much␈α⊂simpler␈α⊂than␈α⊂LISP␈α⊂in␈α⊂its␈α⊂basic␈α⊂structure,␈α⊂and␈α⊃its␈α⊂well-formed
␈↓ ↓H␈↓formulas (abbreviated wffs) are constructed as follows:

␈↓ ↓H␈↓        1. A variable is a wff.

␈↓ ↓H␈↓        2. If ␈↓↓f␈↓ and ␈↓↓e␈↓ are wffs, then so is ␈↓↓f(e).␈↓

␈↓ ↓H␈↓        3. If ␈↓↓v␈↓ is a variable and ␈↓↓e␈↓ is a wff, then ␈↓↓(λv.e)␈↓ is a wff.

␈↓ ↓H␈↓        4. An expression is a wff only if its being a wff follows from the above rules.

␈↓ ↓H␈↓        Here are some examples.

␈↓ ↓H␈↓        1. ␈↓↓x␈↓ and ␈↓↓y␈↓ are wffs by rule 1.

␈↓ ↓H␈↓        2.␈α
␈↓↓x(x),␈↓␈α∞␈↓↓x(y),␈↓␈α
␈↓↓y(x)␈↓␈α
and␈α∞␈↓↓(x(y))(x)␈↓␈α
are␈α∞wffs.␈α
 The␈α
same␈α∞symbol␈α
can␈α
and␈α∞often␈α
does␈α∞appear␈α
in
␈↓ ↓H␈↓both function and argument positions.

␈↓ ↓H␈↓        3.␈α␈↓↓(λx.(λy.x)),␈↓␈α␈↓↓(λx.(λy.y))␈↓␈αand␈α␈↓↓(λf.(λx.f(x(x)))(λx.f(x(x))))␈↓␈αare␈αall␈αwffs␈αthat␈αwill␈αbe␈αimportant
␈↓ ↓H␈↓in subsequent developments.

␈↓ ↓H␈↓        The␈α∩occurrences␈α∩of␈α∪variables␈α∩in␈α∩a␈α∪λ-expression␈α∩may␈α∩be␈α∪divided␈α∩into␈α∩free␈α∪and␈α∩bound
␈↓ ↓H␈↓occurrences.␈α⊂ Any␈α⊂occurrence␈α⊂of␈α⊂␈↓↓x␈↓␈α⊂within␈α⊂an␈α⊂expression␈α⊂␈↓↓(λx.exp)␈↓␈α⊂is␈α⊂a␈α⊂bound␈α⊂occurrence.␈α∂ The
␈↓ ↓H␈↓expression␈αrepresented␈αby␈α␈↓↓exp␈↓␈αis␈αcalled␈αthe␈αscope␈αof␈αthis␈αoccurrence␈αof␈α␈↓↓λx.␈↓␈α Other␈αoccurrences␈αare
␈↓ ↓H␈↓called␈αfree,␈αand␈αsometimes␈αthe␈αvariables␈αthemselves␈αare␈αcalled␈αfree␈αor␈αbound.␈α This␈αis␈αa␈αmisnomer,
␈↓ ↓H␈↓because␈α∂a␈α∂given␈α∞variable␈α∂may␈α∂have␈α∂both␈α∞free␈α∂and␈α∂bound␈α∂occurrences␈α∞in␈α∂a␈α∂particular␈α∂wff.␈α∞ An
␈↓ ↓H␈↓occurrence␈α∞of␈α∞a␈α
variable␈α∞␈↓↓x␈↓␈α∞is␈α∞called␈α
bound␈α∞by␈α∞␈↓↓λx␈↓␈α
in␈α∞␈↓↓λx.exp␈↓␈α∞if␈α∞it␈α
is␈α∞free␈α∞in␈α
␈↓↓exp.␈↓␈α∞ In␈α∞the␈α∞last␈α
λ-
␈↓ ↓H␈↓expression in example 3 above, each ␈↓↓λx␈↓ binds two occurrences of ␈↓↓x.␈↓

␈↓ ↓H␈↓        Just␈α∂as␈α∂in␈α∂LISP␈α∂or␈α∂in␈α∂logic␈α∂or␈α∂in␈α∂definite␈α∂integrals␈α∂in␈α∂calculus,␈α∂bound␈α∂variables␈α⊂may␈α∂be
␈↓ ↓H␈↓changed␈αwithout␈αchanging␈αthe␈αmeaning␈αof␈αthe␈α
expression␈αprovided␈αall␈αoccurrences␈αin␈αthe␈αscope␈α
of
␈↓ ↓H␈↓a␈α∂given␈α∂variable␈α∂binder␈α∂are␈α∂changed␈α∂and␈α∞no␈α∂variable␈α∂that␈α∂is␈α∂free␈α∂in␈α∂a␈α∂subexpression␈α∞becomes
␈↓ ↓H␈↓bound.␈α∂ Thus␈α⊂we␈α∂may␈α⊂change␈α∂␈↓↓(λx.(λy.x))␈↓␈α⊂to␈α∂␈↓↓(λu.(λy.u))␈↓␈α⊂without␈α∂changing␈α⊂the␈α∂meaning␈α⊂of␈α∂the
␈↓ ↓H␈↓expression.␈α∞ However,␈α∞we␈α∞could␈α∞not␈α∂change␈α∞the␈α∞␈↓↓x␈↓␈α∞in␈α∞␈↓↓(λx.(λy.y))␈↓␈α∂to␈α∞␈↓↓y␈↓␈α∞without␈α∞changing␈α∞the␈α∂␈↓↓y␈↓␈α∞to
␈↓ ↓H␈↓something␈αelse␈αfirst,␈αbecause␈αthis␈αwould␈αgive␈α␈↓↓(λy.(λy.y))␈↓␈αwhich␈αreplaces␈αthe␈αsecond␈αoccurrence␈αof␈α␈↓↓x␈↓
␈↓ ↓H␈↓by␈αa␈α
variable␈αwhich␈αis␈α
now␈αbound␈αby␈α
the␈αsecond␈α
λ.␈α This␈αkind␈α
of␈αchange␈αof␈α
variables␈αis␈αcalled␈α
an
␈↓ ↓H␈↓alphabetic change and is also referred to as α-conversion.

␈↓ ↓H␈↓        The␈αsecond␈αkind␈αof␈αconversion␈αis␈αλ-conversion.␈α It␈α
can␈αbe␈αdone␈αwhen␈αa␈αwff␈αconsists␈αof␈αa␈α
λ-
␈↓ ↓H␈↓expression␈α∃applied␈α∃to␈α∃another␈α∃wff.␈α∃ An␈α⊗example␈α∃is␈α∃␈↓↓(λx.x(y))(u),␈↓␈α∃and␈α∃the␈α∃general␈α⊗form␈α∃is
␈↓ ↓H␈↓␈↓↓(λx.e1)(e2).␈↓␈α The␈αconversion␈αconsists␈αessentially␈αin␈αreplacing␈αthe␈αgiven␈αexpression␈αby␈αthe␈αresult␈αof
␈↓ ↓H␈↓substituting ␈↓↓e2␈↓ for ␈↓↓x␈↓ in ␈↓↓e1.␈↓  Thus the above-mentioned ␈↓↓(λx.x(y))(u)␈↓ converts to ␈↓↓u(y).␈↓

␈↓ ↓H␈↓        There␈α∞is␈α
a␈α∞catch.␈α∞ Suppose␈α
we␈α∞want␈α
to␈α∞convert␈α∞␈↓↓(λx.(λy.x(y)))(y(y)).␈↓␈α
 If␈α∞we␈α∞simply␈α
subsitute
␈↓ ↓H␈↓␈↓↓y(y)␈↓␈αfor␈α␈↓↓x␈↓␈αin␈α␈↓↓(λy.x(y)),␈↓␈α
the␈αfree␈αoccurrences␈αof␈α␈↓↓y␈↓␈αin␈α
␈↓↓y(y)␈↓␈αwill␈αbecome␈αbound␈αgiving␈α␈↓↓(λy.y(y)(y)),␈↓␈α
and
␈↓ ↓H␈↓this␈αisn't␈αallowed,␈α
because␈αit␈αwould␈αchange␈α
the␈αintended␈αmeaning␈αof␈α
the␈αλ-expression.␈α When␈αa␈α
λ-
␈↓ ↓H␈↓conversion␈αwill␈αresult␈αin␈αthe␈α"capture"␈αof␈αa␈αfree␈α
occurrence␈αof␈αa␈αvariable,␈αit␈αmust␈αbe␈αpreceded␈αby␈α
a
␈↓ ↓H␈↓change␈α∞of␈α∞bound␈α∂variables.␈α∞ In␈α∞the␈α∞above␈α∂example,␈α∞we␈α∞can␈α∞replace␈α∂the␈α∞bound␈α∞occurrences␈α∂of␈α∞␈↓↓y␈↓
␈↓ ↓H␈↓before␈αdoing␈αthe␈αλ-conversion␈αand␈αget␈αfirst␈α␈↓↓(λx.(λu.x(u)))(y(y))␈↓␈αand␈αthen␈α␈↓↓(λu.y(y)(u)).␈↓␈α In␈αthinking
␈↓ ↓H␈↓about␈α∀programs␈α∀to␈α∀do␈α∀λ-conversion,␈α∀it␈α∀is␈α∀usually␈α∀convenient␈α∀to␈α∀regard␈α∀the␈α∃preliminary␈α∀α-
␈↓ ↓H␈↓conversion that may be needed as part of the λ-conversion rather than as a precondition.
␈↓ ↓H␈↓␈↓ ¬wChapter  XI␈↓ 96


␈↓ ↓H␈↓        We␈α∂write␈α∞␈↓↓e1 → e2␈↓␈α∂as␈α∞a␈α∂way␈α∞of␈α∂saying␈α∞that␈α∂␈↓↓e1␈↓␈α∞converts␈α∂to␈α∞␈↓↓e2.␈↓␈α∂ We␈α∞include␈α∂conversions␈α∞of
␈↓ ↓H␈↓subexpressions as λ-conversions.  Here are some examples of λ-conversion.

␈↓ ↓H␈↓        ␈↓↓(λx.(λy.x))(a)(b) → (λy.a)(b) → a␈↓

␈↓ ↓H␈↓        ␈↓↓(λx.(λy.y))(a)(b) → (λy.y)(b) → b␈↓

␈↓ ↓H␈↓        ␈↓↓(λx.f(x(x)))(λx.f(x(x))) → f(λx.f(x(x)))(λx.f(x(x))))␈↓.

␈↓ ↓H␈↓Each of them will be important.

␈↓ ↓H␈↓        A␈α∩wff␈α∩which␈α∪is␈α∩not␈α∩subject␈α∩to␈α∪λ-conversion␈α∩is␈α∩said␈α∩to␈α∪be␈α∩in␈α∩normal␈α∩form.␈α∪ Some␈α∩λ-
␈↓ ↓H␈↓expressions␈α∂can␈α∂be␈α∂converted␈α⊂successively␈α∂0␈α∂or␈α∂more␈α∂times␈α⊂and␈α∂will␈α∂eventually␈α∂reach␈α⊂a␈α∂normal
␈↓ ↓H␈↓form.␈α
 The␈α
first␈α∞two␈α
conversions␈α
above␈α
are␈α∞reductions␈α
to␈α
a␈α
normal␈α∞form.␈α
 The␈α
third␈α∞example␈α
is
␈↓ ↓H␈↓not␈α
reduced␈α
to␈αnormal␈α
form,␈α
and␈αit␈α
is␈α
is␈α
clear␈αthat␈α
it␈α
can't␈αbe,␈α
because␈α
the␈αargument␈α
of␈α
␈↓↓f␈↓␈α
on␈αthe
␈↓ ↓H␈↓right is just the whole expression on the left.  We have

␈↓ ↓H␈↓        ␈↓↓e → f(e) → f(f(e)) → f(f(f(e))) →␈↓ etc.

␈↓ ↓H␈↓        Sometimes␈α
a␈α
wff␈α
may␈α
be␈α
convertible␈αin␈α
several␈α
ways,␈α
because␈α
several␈α
of␈α
its␈αsubexpressions
␈↓ ↓H␈↓may␈αbe␈αapplications␈αof␈αa␈αλ-expression␈αto␈αanother␈αexpression.␈α Whether␈αa␈αnormal␈αform␈αis␈αreached
␈↓ ↓H␈↓may␈αdepend␈α
on␈αthe␈αorder␈α
in␈αwhich␈αreductions␈α
are␈αdone.␈α However,␈α
the␈αChurch-Rosser␈αtheorem␈α
of
␈↓ ↓H␈↓1936␈α⊂asserts␈α⊂that␈α⊂if␈α⊂a␈α⊂normal␈α⊂form␈α⊂is␈α⊂reached␈α⊂by␈α⊂some␈α⊂sequence␈α⊂of␈α⊂conversions,␈α⊂it␈α⊃is␈α⊂unique;
␈↓ ↓H␈↓different␈α∞conversion␈α∞paths␈α
cannot␈α∞give␈α∞rise␈α
to␈α∞different␈α∞normal␈α
forms.␈α∞ It␈α∞can␈α∞happen,␈α
however,
␈↓ ↓H␈↓that some paths give a normal form and others don't.

␈↓ ↓H␈↓        Church␈α⊃originally␈α∩proposed␈α⊃the␈α⊃λ-calculus␈α∩as␈α⊃a␈α⊃way␈α∩of␈α⊃formalizing␈α⊃the␈α∩foundations␈α⊃of
␈↓ ↓H␈↓mathematics,␈αand␈αthe␈αoriginal␈αversion␈αincluded␈αlogical␈αoperations␈αand␈αquantifiers.␈α Unfortunately,
␈↓ ↓H␈↓this␈αsystem␈αproved␈αinconsistent␈α(any␈αformula␈αwas␈αprovable)␈αand␈αhad␈αto␈αbe␈αabandoned.␈α However,
␈↓ ↓H␈↓Church␈α⊂was␈α⊂able␈α⊂to␈α⊂show␈α⊂that␈α⊂arithmetic␈α⊂computations␈α⊂could␈α⊂be␈α⊂encoded␈α⊂as␈α⊂reductions␈α⊂of␈α⊂λ-
␈↓ ↓H␈↓expressions␈α⊂to␈α⊂normal␈α⊂form,␈α⊂and␈α⊂it␈α⊂was␈α⊂shown␈α⊂in␈α⊂the␈α⊂1930s␈α⊂that␈α⊂λ-computations␈α⊃and␈α⊂Turing
␈↓ ↓H␈↓machine computations were equally powerful.

␈↓ ↓H␈↓        When␈α⊂we␈α⊂compare␈α⊂reduction␈α⊂of␈α⊂λ-expressions␈α⊂to␈α⊂normal␈α⊂form␈α⊂to␈α⊂LISP␈α⊃computations,␈α⊂it
␈↓ ↓H␈↓seems␈αsurprising␈α
that␈αany␈α
significant␈αcomputing␈α
can␈αbe␈α
done␈αwith␈α
only␈αλ-conversion.␈α
 There␈αare
␈↓ ↓H␈↓apparently␈αno␈αlists,␈αno␈α␈↓αa|␈↓,␈α␈↓αd|␈↓or␈α␈↓↓cons,␈↓␈αno␈αconditional␈αexpressions␈αand␈αno␈αrecursion.␈α However,␈αas␈αwe
␈↓ ↓H␈↓shall␈α
now␈αshow␈α
all␈αthese␈α
things␈α
can␈αbe␈α
done␈αin␈α
the␈α
λ-calculus.␈α While␈α
Church␈αfirst␈α
showed␈αhow␈α
to
␈↓ ↓H␈↓do␈α∂computation␈α∂in␈α∂λ-calculus,␈α∂the␈α∂most␈α⊂straightforward␈α∂and␈α∂instructive␈α∂course␈α∂for␈α∂us␈α∂is␈α⊂to␈α∂use
␈↓ ↓H␈↓constructions due essentially to Dana Scott that imitate pure LISP.

␈↓ ↓H␈↓        First␈α∀we␈α∀need␈α∪a␈α∀slightly␈α∀abbreviated␈α∪notation.␈α∀ All␈α∀our␈α∪functions␈α∀have␈α∀had␈α∀just␈α∪one
␈↓ ↓H␈↓argument,␈α∂but␈α∂the␈α∂value␈α∂of␈α∂a␈α∂function␈α⊂can␈α∂be␈α∂another␈α∂function,␈α∂and␈α∂this␈α∂is␈α∂enough␈α⊂to␈α∂imitate
␈↓ ↓H␈↓functions␈α
of␈α
several␈α
arguments.␈α
 The␈αidea␈α
is␈α
to␈α
regard␈α
␈↓↓f(x,y)␈↓␈αas␈α
just␈α
an␈α
abbreviation␈α
of␈α␈↓↓f(x)(y),␈↓␈α
i.e.
␈↓ ↓H␈↓to␈αregard␈αa␈αfunction␈αof␈α
two␈αarguments␈αas␈αa␈αfunction␈α
of␈αone␈αargument␈α(the␈αfirst␈α
argument)␈αwhose
␈↓ ↓H␈↓value␈α
is␈α
a␈α
function␈α
of␈αone␈α
argument␈α
(the␈α
second␈α
argument).␈α We␈α
then␈α
also␈α
regard␈α
␈↓↓(λx y.e)␈↓␈α
as␈αan
␈↓ ↓H␈↓abbreviation␈α
of␈α
␈↓↓(λx.(λy.e)).␈α
 ␈↓␈α       We␈α
now␈α
proceed␈α
by␈αidentifying␈α
certain␈α
objects␈α
and␈αfunctions
␈↓ ↓H␈↓of LISP as certain λ-expressions.

␈↓ ↓H␈↓        We begin with truth values and write

␈↓ ↓H␈↓        ␈↓↓true = (λx y.x) = (λx.(λy.x))␈↓
␈↓ ↓H␈↓␈↓ ¬wChapter  XI␈↓ 97


␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓↓false = (λx y.y) = (λx.(λy.x))␈↓.

␈↓ ↓H␈↓So␈α
far␈α
this␈α
is␈α
quite␈α
arbitrary,␈α
and␈αthe␈α
motivation␈α
for␈α
these␈α
identifications␈α
is␈α
not␈α
apparent.␈α Now
␈↓ ↓H␈↓we do conditional expressions and write

␈↓ ↓H␈↓        ␈↓↓␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = p(a)(b) = p(a,b)␈↓,

␈↓ ↓H␈↓and we already get a return from our investment.  Namely,

␈↓ ↓H␈↓        ␈↓↓␈↓αif␈↓↓ true ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = true(a)(b) = (λx y.x)(a,b) → a␈↓,

␈↓ ↓H␈↓which is just the property this conditional expression should have.  Likewise

␈↓ ↓H␈↓        ␈↓↓␈↓αif␈↓↓ false ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = false(a)(b) = (λx y.y)(a,b) → b␈↓.

␈↓ ↓H␈↓Using this conditional expression notation, we can define the propositional connectives as

␈↓ ↓H␈↓        ␈↓↓p ∧ q = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ false = p(q,false)␈↓

␈↓ ↓H␈↓        ␈↓↓p ∨ q = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ true ␈↓αelse␈↓↓ q = p(true,q)␈↓

␈↓ ↓H␈↓        ␈↓↓¬p = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ false ␈↓αelse␈↓↓ true = p(false,true)␈↓,

␈↓ ↓H␈↓and␈α⊃all␈α⊃the␈α⊂usual␈α⊃truth␈α⊃table␈α⊂reductions␈α⊃immediately␈α⊃follow␈α⊂by␈α⊃reducing␈α⊃the␈α⊃λ-expressions␈α⊂to
␈↓ ↓H␈↓normal form.  For example

␈↓ ↓H␈↓        ␈↓↓true ∧ false = true(false,false) = (λx y.x)(false,false) → false␈↓.

␈↓ ↓H␈↓It␈α≤is␈α≤important␈α≤to␈α≤notice␈α≤that␈α≤this␈α≤only␈α≤works␈α≤if␈α≤the␈α≤propositional␈α≤argument␈α≤␈↓↓p␈↓␈α≤of
␈↓ ↓H␈↓"␈↓↓␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b␈↓"␈αconverts␈αto␈α␈↓↓true␈↓␈αor␈α␈↓↓false.␈↓␈α In␈αLISP␈αanything␈αbut␈α␈↓↓false␈↓␈αbehaves␈αlike␈α␈↓↓true,␈↓␈αbut
␈↓ ↓H␈↓there is no way to make this happen in λ-calculus.

␈↓ ↓H␈↓        Next␈α∃we␈α∃need␈α∃␈↓↓car,␈↓␈α∃␈↓↓cdr␈↓␈α∃and␈α∃␈↓↓cons.␈↓␈α∃ We␈α∃begin␈α∃with␈α∃versions␈α∃that␈α∃meet␈α∃part␈α∃of␈α∃our
␈↓ ↓H␈↓requirements and will use them to construct the final versions.  We write

␈↓ ↓H␈↓        ␈↓↓cons1 = (λ x y z.z(x,y))␈↓

␈↓ ↓H␈↓        ␈↓↓car1 = (λx.x(true))␈↓

␈↓ ↓H␈↓        ␈↓↓cdr1 = (λx.x(false))␈↓,

␈↓ ↓H␈↓which seem mysterious, but it is comforting to observe that

␈↓ ↓H␈↓␈↓ α8␈↓↓car1(cons1(e1,e2))␈↓ ∧8= (λx.x(true))(cons1(e1,e2))␈↓

␈↓ ↓H␈↓␈↓ ∧8␈↓↓→ cons1(e1,e2)(true)␈↓

␈↓ ↓H␈↓␈↓ ∧8␈↓↓= (λx y z.z(x,y))(e1,e2,true)␈↓
␈↓ ↓H␈↓␈↓ ¬wChapter  XI␈↓ 98


␈↓ ↓H␈↓␈↓ ∧8␈↓↓→ true(e1,e2)␈↓

␈↓ ↓H␈↓␈↓ ∧8␈↓↓→ e1␈↓

␈↓ ↓H␈↓        Likewise

␈↓ ↓H␈↓        ␈↓↓cdr1(cons1(e1,e2)) →→ e2␈↓

␈↓ ↓H␈↓where␈α⊃→→␈α⊃refers␈α∩to␈α⊃eventual␈α⊃reduction␈α⊃rather␈α∩than␈α⊃a␈α⊃single␈α⊃step.␈α∩ Thus␈α⊃␈↓↓cons1␈↓␈α⊃has␈α∩one␈α⊃main
␈↓ ↓H␈↓property␈α∩of␈α∩a␈α∩pairing␈α∩operation␈α∩in␈α∩that␈α∩␈↓↓car1␈↓␈α⊃and␈α∩␈↓↓cdr1␈↓␈α∩enable␈α∩us␈α∩to␈α∩get␈α∩the␈α∩operands␈α⊃back.
␈↓ ↓H␈↓However,␈αwe␈α
lack␈αatoms␈α
and␈αa␈α
way␈αof␈α
identifying␈αthem.␈α
 We␈αget␈α
them␈αby␈α
defining␈αan␈α
atom␈α␈↓¬NIL␈↓
␈↓ ↓H␈↓and new λ-expressions ␈↓↓cons,␈↓ ␈↓↓car␈↓ and ␈↓↓cdr.␈↓

␈↓ ↓H␈↓        Our example system will have a single atom ␈↓¬NIL␈↓, and we define

␈↓ ↓H␈↓        ␈↓↓␈↓¬NIL␈↓↓ = cons1(true,true)␈↓

␈↓ ↓H␈↓Now␈α
we␈α
can␈αdefine␈α
a␈α
␈↓↓cons␈↓␈α
that␈αproduces␈α
imitation␈α
S-expressions␈αthat␈α
can␈α
be␈α
distinguished␈αfrom
␈↓ ↓H␈↓our imitation atom ␈↓¬NIL␈↓.

␈↓ ↓H␈↓        ␈↓↓cons = (λx y.cons1(false,(cons1(x,y)))␈↓

␈↓ ↓H␈↓        ␈↓↓car = (λx.car1(cdr1(x)))␈↓

␈↓ ↓H␈↓        ␈↓↓cdr = (λx.cdr1(cdr1(x)))␈↓

␈↓ ↓H␈↓        ␈↓↓null = (λx.car1(x))␈↓.

␈↓ ↓H␈↓The␈α
idea␈α
is␈α
that␈α
the␈αatom␈α
␈↓¬NIL␈↓␈α
has␈α
its␈α
␈↓↓car1␈↓␈α
part␈α␈↓↓true,␈↓␈α
while␈α
every␈α
expression␈α
produced␈α
by␈α␈↓↓cons␈↓␈α
has
␈↓ ↓H␈↓its ␈↓↓car1␈↓ part ␈↓↓false.␈↓  Therefore, we use the ␈↓↓car1␈↓ part in conditional expressions as a test for ␈↓↓null.␈↓

␈↓ ↓H␈↓        Finally, to get recursion, we write

␈↓ ↓H␈↓        ␈↓↓recur = (λf.(λx.f(x(x)))(λx.f(x(x))))␈↓,

␈↓ ↓H␈↓which␈α∀is␈α∀Church's␈α∪famous␈α∀Y␈α∀combinator.␈α∪ The␈α∀property␈α∀that␈α∪makes␈α∀it␈α∀useful␈α∀for␈α∪defining
␈↓ ↓H␈↓recursion, as mentioned above, is that

␈↓ ↓H␈↓        ␈↓↓recur(f) → f(recur(f)) → f(f(recur(f))) → ␈↓etc.

␈↓ ↓H␈↓Notice␈α
that␈α
␈↓↓recur␈↓␈α
is␈α
not␈α
in␈α
normal␈α
form,␈α
since␈α
it␈α
contains␈α
an␈α
application␈α
of␈α
a␈α
λ-expression␈αinside␈α
it.
␈↓ ↓H␈↓Moreover, the above "fixed point" property shows that it has no normal form.

␈↓ ↓H␈↓        Now we can do pure LISP.  We can write

␈↓ ↓H␈↓        ␈↓↓append = recur(λf.(λu v.␈↓αif␈↓↓ null(u) ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ cons(car(u), f(cdr(u),v))))␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓↓equal␈α∃=␈α∃recur(λf.(λx␈α∃y.(null(x)␈α∃∧␈α⊗null(y)␈α∃∨␈α∃(¬null(x)␈α∃∧␈α∃¬null(y))␈α∃∧␈α⊗(f(car(x),car(y))␈α∃∧
␈↓ ↓H␈↓↓f(cdr(x),cdr(y))))))␈↓
␈↓ ↓H␈↓␈↓ ¬wChapter  XI␈↓ 99


␈↓ ↓H␈↓        Using the above abbreviations we can show such facts as

␈↓ ↓H␈↓        ␈↓↓append(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓) → ␈↓¬NIL␈↓↓␈↓

␈↓ ↓H␈↓        ␈↓↓append(cons(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓),␈↓¬NIL␈↓↓) → cons(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓)␈↓

␈↓ ↓H␈↓        ␈↓↓equal(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓) → true␈↓

␈↓ ↓H␈↓        ␈↓↓equal(cons(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓),␈↓¬NIL␈↓↓) → false␈↓.

␈↓ ↓H␈↓The expressions on the right are all abbreviations of normal forms.

␈↓ ↓H␈↓        There␈αare␈αtwo␈αcatches.␈α First,␈αwhile␈αthe␈α
Church-Rosser␈αtheorem␈αassures␈αus␈αthat␈αif␈αwe␈αget␈α
an
␈↓ ↓H␈↓answer␈αit␈α
will␈αbe␈α
unique,␈αit␈αdoesn't␈α
assure␈αus␈α
that␈αall␈αsequences␈α
of␈αreduction␈α
get␈αanswers,␈αand␈α
some
␈↓ ↓H␈↓don't.  Suppose we are computing ␈↓↓append(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓).␈↓¬  We make the abbreviation

␈↓ ↓H␈↓¬        ␈↓↓app1 = ␈↓αif␈↓↓ null(u) ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ cons(car(u),f(cdr(u),v))␈↓¬

␈↓ ↓H␈↓¬and have

␈↓ ↓H␈↓¬␈↓ α8␈↓↓append(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓)␈↓ ∧(= recur(λf u v.app1)(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓)␈↓¬

␈↓ ↓H␈↓¬␈↓ ∧(␈↓↓→ (λf u v.app1)(recur(λf u v.app1))(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓)␈↓¬.

␈↓ ↓H␈↓¬At␈α∩this␈α∩point␈α∩two␈α∩conversions␈α∩are␈α∩possible.␈α∩ We␈α∩could␈α∩convert␈α∩the␈α∩new␈α∪␈↓↓recur(λf␈↓¬␈α∩u
␈↓ ↓H␈↓¬v.app1) or we can convert the application of ␈↓↓λf u v.app1␈↓¬ to its arguments and get

␈↓ ↓H␈↓¬        ␈↓↓→ ␈↓αif␈↓↓ null(␈↓¬NIL␈↓↓) ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓ ␈↓αelse␈↓↓ cons(car(␈↓¬NIL␈↓↓),recur(λf u v.app1)(cdr(␈↓¬NIL␈↓↓),␈↓¬NIL␈↓↓))␈↓¬.

␈↓ ↓H␈↓¬The␈α⊂former␈α⊂could␈α⊂go␈α⊂on␈α⊂indefinitely,␈α⊂while␈α⊂the␈α⊂latter␈α⊂is␈α⊂what␈α⊂imitates␈α⊂the␈α⊂usual
␈↓ ↓H␈↓¬LISP␈α⊂computation␈α⊂and␈α⊂promptly␈α⊂leads␈α⊂to␈α⊂a␈α⊂normal␈α⊂form.␈α⊂ The␈α⊂general␈α⊂rule␈α⊂is␈α⊂to␈α⊂do
␈↓ ↓H␈↓¬first␈α⊂the␈α⊂outermost␈α⊂possible␈α⊂reduction.␈α⊂ It␈α⊂can␈α⊂be␈α⊂shown␈α⊂that␈α⊂this␈α⊂rule␈α⊂leads␈α⊂to
␈↓ ↓H␈↓¬a␈α∪normal␈α∪form␈α∩whenever␈α∪a␈α∪normal␈α∩form␈α∪exists.␈α∪ It␈α∩corresponds␈α∪to␈α∪a␈α∩call-by-name
␈↓ ↓H␈↓¬evaluation rule.

␈↓ ↓H␈↓¬        The␈α⊃preceding␈α⊃shows␈α⊃how␈α∩to␈α⊃translate␈α⊃any␈α⊃pure␈α∩LISP␈α⊃function␈α⊃as␈α⊃a␈α∩wff␈α⊃of
␈↓ ↓H␈↓¬λ-calculus.␈α⊃ If␈α⊃we␈α⊃also␈α∩encode␈α⊃its␈α⊃arguments␈α⊃and␈α∩form␈α⊃the␈α⊃wff␈α⊃consisting␈α∩of␈α⊃the
␈↓ ↓H␈↓¬application␈α∪of␈α∪the␈α∪function␈α∪to␈α∪its␈α∪arguments␈α∪and␈α∪then␈α∪normalize␈α∪␈↓↓e,␈↓¬␈α∪the␈α∩process
␈↓ ↓H␈↓¬will␈α⊗terminate␈α↔provided␈α⊗the␈α↔LISP␈α⊗computation␈α⊗taken␈α↔in␈α⊗the␈α↔call-by-name␈α⊗sense
␈↓ ↓H␈↓¬terminates,␈α∩and␈α∪the␈α∩resulting␈α∪normal␈α∩form␈α∪will␈α∩be␈α∪an␈α∩encoding␈α∪of␈α∩the␈α∪result␈α∩of
␈↓ ↓H␈↓¬the LISP computation.

␈↓ ↓H␈↓¬        The␈α∃second␈α⊗catch␈α∃is␈α∃that␈α⊗the␈α∃λ-calculus␈α∃provides␈α⊗no␈α∃way␈α∃of␈α⊗making␈α∃or
␈↓ ↓H␈↓¬proving␈α⊃general␈α⊃statements.␈α⊃ While␈α⊃every␈α⊃individual␈α⊃case␈α⊃of␈α⊂␈↓↓append(append(u,v),w)␈↓¬
␈↓ ↓H␈↓¬will␈α→reduce␈α→to␈α_the␈α→same␈α→normal␈α_form␈α→as␈α→␈↓↓append(u,append(v,w))␈↓¬,␈α→the␈α_λ-calculus
␈↓ ↓H␈↓¬provides␈α∀no␈α∀way␈α∪of␈α∀stating␈α∀or␈α∪proving␈α∀it␈α∀within␈α∪the␈α∀formalism.␈α∀ Of␈α∀course,␈α∪it
␈↓ ↓H␈↓¬isn't␈α≡hard␈α≡to␈α≡show␈α∨by␈α≡informal␈α≡reasoning␈α≡␈↓↓about␈↓¬␈α≡the␈α∨λ-calculus.␈α≡ Church's
␈↓ ↓H␈↓¬original 1920s inconsistent formalism did provide for general statements.

␈↓ ↓H␈↓¬        Here are some remarks.

␈↓ ↓H␈↓¬        1.␈α∪Reducing␈α∪to␈α∪normal␈α∀form␈α∪even␈α∪simple␈α∪imitation␈α∪LISP␈α∀expressions␈α∪like
␈↓ ↓H␈↓¬␈↓↓append(cons(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓),cons(␈↓¬NIL␈↓↓,␈↓¬NIL␈↓↓)),␈↓¬␈α∀i.e.␈α∪imitating␈α∀the␈α∪computation␈α∀of␈α∀␈↓↓(␈↓¬NIL␈↓↓)*(␈↓¬NIL␈↓↓)␈α∪=
␈↓ ↓H␈↓↓(␈↓¬NIL␈↓↓␈α↔␈↓¬NIL␈↓↓)␈↓¬,␈α⊗is␈α↔a␈α⊗long␈α↔computation␈α⊗best␈α↔done␈α⊗by␈α↔a␈α⊗λ-calculus␈α↔reduction␈α⊗program
␈↓ ↓H␈↓¬written in LISP.
␈↓ ↓H␈↓␈↓ ¬wChapter  XI␈↓ *10


␈↓ ↓H␈↓¬        2.␈α∀Further␈α∃definitions␈α∀could␈α∀give␈α∃an␈α∀improved␈α∀language␈α∃for␈α∀LISP␈α∃in␈α∀λ-
␈↓ ↓H␈↓¬calculus.␈α∩ One␈α∩way␈α∪to␈α∩get␈α∩more␈α∪atoms␈α∩is␈α∩to␈α∩regard␈α∪a␈α∩certain␈α∩class␈α∪of␈α∩composite
␈↓ ↓H␈↓¬expressions formed with ␈↓↓cons1␈↓¬ as atoms just as we did with ␈↓↓␈↓¬NIL␈↓↓.␈↓¬

␈↓ ↓H␈↓¬        3.␈α∪The␈α∪LISP␈α∪in␈α∪λ-calculus␈α∪formalism␈α∪works␈α∪only␈α∪if␈α∪all␈α∪expressions␈α∩that
␈↓ ↓H␈↓¬occur␈α⊃in␈α∩the␈α⊃computation␈α∩are␈α⊃constructed␈α∩in␈α⊃the␈α∩manner␈α⊃provided␈α∩for.␈α⊃ Including
␈↓ ↓H␈↓¬general␈α∀λ-expressions␈α∃even␈α∀as␈α∀list␈α∃elements␈α∀can␈α∀cause␈α∃strange␈α∀results␈α∃when␈α∀an
␈↓ ↓H␈↓¬attempt is made to normalize them.

␈↓ ↓H␈↓¬        4.␈α∩While␈α⊃encoding␈α∩LISP␈α∩in␈α⊃λ-calculus␈α∩shows␈α⊃that␈α∩λ-calculus␈α∩is␈α⊃universal
␈↓ ↓H␈↓¬in␈α⊗its␈α⊗computing␈α⊗capabilities,␈α⊗this␈α⊗doesn't␈α↔seem␈α⊗to␈α⊗be␈α⊗a␈α⊗good␈α⊗way␈α↔of␈α⊗taking
␈↓ ↓H␈↓¬advantage of the ability of the λ-calculus to express functions of higher type.
␈↓ ↓H␈↓␈↓ εH␈↓ ?i


␈↓ ↓H␈↓α␈↓ ¬=FUNCTION INDEX

␈↓ ↓H␈↓loop   2
␈↓ ↓H␈↓neval   1
␈↓ ↓H␈↓nevcond   2
␈↓ ↓H␈↓nprup   2
␈↓ ↓H␈↓ta   4
␈↓ ↓H␈↓terma   3
␈↓ ↓H␈↓termastar   3
␈↓ ↓H␈↓t␈↓β1␈↓   4
␈↓ ↓H␈↓␈↓ εH␈↓ ?i


␈↓ ↓H␈↓α␈↓ ¬DDEFINED LABELS

␈↓ ↓H␈↓cbneval   1
␈↓ ↓H␈↓lambda   4
␈↓ ↓H␈↓loop forever   2
␈↓ ↓H␈↓neval    1
␈↓ ↓H␈↓nevcond    2
␈↓ ↓H␈↓noncomput   2
␈↓ ↓H␈↓nprup    2
␈↓ ↓H␈↓ta    4
␈↓ ↓H␈↓terma    3
␈↓ ↓H␈↓termastar    3
␈↓ ↓H␈↓t␈↓β1␈↓    4